$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$), $L$:(event{-}info(${\it ds}$;${\it da}$) List).
\\[0ex](ecl{-}halt(${\it ds}$;${\it da}$;$x$)(0,$L$))
\\[0ex]$\Rightarrow$ ($\uparrow$isl(ecl{-}halt{-}kind($x$)))
\\[0ex]$\Rightarrow$ ((last($L$).1) = outl(ecl{-}halt{-}kind($x$)) $\in$ Knd)